Equivalence of Deterministic Top-Down Tree-to-String Transducers is Decidable

摘要

We show that equivalence of deterministic top-down tree-to-string transducersis decidable, thus solving a long standing open problem in formal languagetheory. We also present efficient algorithms for subclasses: polynomial timefor total transducers with unary output alphabet (over a given top-down regulardomain language), and co-randomized polynomial time for linear transducers;these results are obtained using techniques from multi-linear algebra. For our main result, we prove that equivalence can be certified by means ofinductive invariants using polynomial ideals. This allows us to construct twosemi-algorithms, one searching for a proof of equivalence, one for a witness ofnon-equivalence. Furthermore, we extend our result to deterministic top-downtree-to-string transducers which produce output not in a free monoid but in afree group.